Iof proof for Lemma mul com:
a, b:
. (a * b) = (b * a)
by (Auto_aux (first_nat 1:n) ((first_nat 2:n),(first_nat 3:n)) (first_tok :t) inil_term)
.| 12,41 |
a, b:. (a * b) = (b * a)
by (Auto_aux (first_nat 1:n) ((first_nat 2:n),(first_nat 3:n)) (first_tok :t) inil_term)
.
| Definitions |  Tx:A. B(x) |